(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun k () Real)
(declare-fun p () Real)
(declare-fun u () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(assert (exists ((h Real)) (= (= d 0) (= (> 0 (- (/ 6 a))) (= (and (< u d) (< (/ h 0) 0)) (= f 2))))))
(assert (forall ((g Real)) (= (> (/ 1 k e) 0 b) (= (/ 5 c) (/ 0 (- 9 (* (* (- 5 v) (- 8 (* w u) (+ 1 u))) (- (+ 2 (/ 1 w) k))))) (* 35 (* (+ (* v w) k) k)) c))))
(assert (= w (- u p) k))
(check-sat)
